Abstract interpretation is a theory for approximating the semantics of systems, such as computer programs and industrial designs, based on monotonic functions over ordered sets, especially lattices. Abstract interpretation can be viewed as a partial execution of a computer program that gains information about its semantics (e.g., control structure and flow of information) without performing all the calculations of the program. Abstract interpretation computes fixpoints for programs that each represent a state of the abstract interpretation of the program at some point or step of interpretation. Abstract interpretation can be used to determine whether a program satisfies a condition (e.g., the value of variable B is never greater than 100). If all fixpoints computed by an abstract interpretation of the program satisfy the condition, then all concrete behaviors of the program satisfy the condition. If a fixpoint, however, does not satisfy the condition, then there are two possibilities. First, the program does not satisfy the condition, and a “true error” in the program has been found. Second, the program satisfies the condition but the abstract interpretation was not precise enough to verify it, and a “false error” in the program has been found. Abstract interpretations represent programs with varying degrees of precision to accommodate programs with infinite domains or to efficiently accommodate very large programs. If the precision is too low, the abstract interpretation will, however, detect many false errors, which reduces its usability.
Predicate abstraction is a form of abstract interpretation in which concrete states are abstracted by their valuation to a finite set of predicates. Several tools are available that use predicate abstraction to verify finite state interface protocols on programs. To reduce false errors, these tools typically analyze an abstract counterexample to check whether the counterexample is feasible in the concrete program. A counterexample indicates that the condition of the program is not satisfied. If the counterexample is feasible, the tools add more predicates to improve the precision of the predicate abstraction. This process, referred to as “counterexample driven refinement,” continues iteratively until (1) the condition is proved, (2) a true error is found, or (3) resources (e.g., time or memory) are exhausted.
Abstract interpretations generally operate over mathematical lattices and compute the semantics of programs as fixpoints. Such fixpoint computations may not converge, however, if the lattice has infinite ascending chains. To ensure convergence of fixpoints, abstract interpretations use a “widening” technique to over-approximate the semantics. The widening operator ∇ has the property that for all states x and y the result x∇y is greater than both x and y. Furthermore, widening guarantees convergence of fixpoint computation in that in any infinite increasing sequence x0, x1, x2, . . . , the sequence y0, y1, y2, . . . , given by y0=x0 and yi+1=yi∇(yi∪xi+1) is guaranteed to converge.